#pragma once
#include "PDTExp.h"
#include "PDTVar.h"
#include "PDTNumConst.h"
#include "PDTBoolConst.h"
#include "PDTAssign.h"
#include "PDTSequenceOp.h"

class PDTQuantifier: public PDTExpBool {
    unsigned int varCount;
public:
	PDTQuantifier(PDTCodeGraph & CG, vector<PDTVar*> & vars, PDTExpBool & exp) :
		PDTExpBool(CG), varCount(vars.size()) {
		for (unsigned int i = 0; i < vars.size(); i++) {
			PDTVar * var = vars[i];
			PDTNode * node = var->getNode();
			addChild(node);
			node->addParent(this);
		}
		addChild(&exp);
		exp.addParent(this);
	}
	virtual bool isQuantifier() {
		return true;
	}

	PDTNode * getVarNode(int i) const {
		return children[i];
	}

	unsigned int getNumVars() const {
        return varCount;
	}

	PDTExpBool * getExpBool() const {
		int expIdx = children.size() - 1;
		return dynamic_cast<PDTExpBool*> (children[expIdx]);
	}

	virtual stringstream & toString(stringstream & ss) const {
		int numVars = getNumVars();
		for (int i = 0; i < numVars; i++) {
			ss << "(";
			PDTNode * var = getVarNode(i);
			var->toString(ss);
			ss << " ";
			if (var->isSetVar()) {
				PDTSetVar * sVar = dynamic_cast<PDTSetVar*> (var);
				ss << ": ";
				PDTSet * set = sVar->getSet();
				if (set != NULL)
					set->toString(ss);
			} else if (var->isVar()) {
				PDTVar * varptr = dynamic_cast<PDTVar*>(var);
				if (varptr->isBound()) {
					ss << ":";
					varptr->getRange()->toString(ss);
				}
			}
			ss << ") ";
		}
		ss << "._ ( ";
		PDTNode * exp = getExpBool();
		exp->toString(ss);
		ss << ")";
		return ss;
	}
};

class PDTForall :  public PDTQuantifier, public TraverseIfc <PDTForall, PDTNode> { public: TRAVERSAL_IFC_IMPL(PDTForall)
public:
	PDTForall(PDTCodeGraph & CG, vector<PDTVar*> & vars, PDTExpBool & exp) :
		PDTQuantifier(CG, vars, exp) {
	}

	NodeTypeEnum getType() {
		return PDTForall_Em;
	}
	virtual bool isForall() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		PDTExp * exp = getExpBool();  //Get the boolean expression
		for (unsigned int i = 0; i<getNumVars(); i++)
		{
			PDTNode * var = getVarNode(i); //the variables involved
			if (var->isNumVar())
			{
				PDTNumVar* numVar = dynamic_cast<PDTNumVar*>(var);
				PDTIntRange * varRange = numVar->getRange();   //find the range of variable
				varRange->getStart()->eval(CG);
				int start = (dynamic_cast<PDTNumConstInt*>(varRange->getStart()->nValue))->getValue();
				varRange->getEnd()->eval(CG);
				int end = (dynamic_cast<PDTNumConstInt*>(varRange->getEnd()->nValue))->getValue();
				string varName = (numVar->getName()).substr(8,1);
				PDTVar* temp = exp->searchForVariable(varName);
				PDTNumVar* varFound = dynamic_cast<PDTNumVar*>(temp);  //search for the variable
				for (int i = start; i<=end; i++)
				{
					PDTNumConstInt eye(CG,i);
					PDTAssign assignI(CG, *varFound, eye); //do the assignments
					assignI.eval(CG);
					exp->eval(CG); //then evaluate
					bool result = (dynamic_cast<PDTBoolConst*>(exp->nValue))->getValue();
					if (!result) //depending on the result, we evaluate the quantifier
					{
						cout<<"Quantifier for all is not satisfied"<<endl;
						nValue = new PDTBoolConst(CG, false);
						return true;
					}
				}
			}
		}

		cout<<"Quantifier for all satisfied"<<endl;
		nValue = new PDTBoolConst(CG, true);
		return true;
	}

	//// Not to be used for now ////
	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		vector<PDTVar*> varsClone;
		for (unsigned int i = 0; i<getNumVars(); i++)
			varsClone.push_back(dynamic_cast<PDTVar*>(getVarNode(i)->clone(CG)));

		PDTExpBool* expClone = (PDTExpBool*)getExpBool()->clone(CG);
		toReturn = new PDTForall(CG, varsClone, *expClone);
		return toReturn;
	}
	//////////////////////////////////

	virtual stringstream & toString(stringstream & ss) const {
		ss << "Forall ";
		PDTQuantifier::toString(ss);
		return ss;
	}
};

class PDTExist :  public PDTQuantifier, public TraverseIfc <PDTExist, PDTNode> 
{ public:  TRAVERSAL_IFC_IMPL(PDTExist)
public:
	PDTExist(PDTCodeGraph & CG, vector<PDTVar*> & vars, PDTExpBool & exp) :
		PDTQuantifier(CG, vars, exp) {

	}
	NodeTypeEnum getType() {
		return PDTExist_Em;
	}
	virtual bool isExist() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		PDTExp * exp = getExpBool();
		for (unsigned int i = 0; i<getNumVars(); i++)
		{
			PDTNode * var = getVarNode(i);
			if (var->isNumVar())
			{
				PDTNumVar* numVar = dynamic_cast<PDTNumVar*>(var);
				PDTIntRange * varRange = numVar->getRange();
				varRange->getStart()->eval(CG);
				int start = (dynamic_cast<PDTNumConstInt*>(varRange->getStart()->nValue))->getValue();
				varRange->getEnd()->eval(CG);
				int end = (dynamic_cast<PDTNumConstInt*>(varRange->getEnd()->nValue))->getValue();
				string varName = (numVar->getName()).substr(8,1);
				PDTVar* temp = exp->searchForVariable(varName);
				PDTNumVar* varFound = dynamic_cast<PDTNumVar*>(temp);
				for (int i = start; i<=end; i++)
				{
					PDTNumConstInt eye(CG,i);
					PDTAssign assignI(CG, *varFound, eye);
					assignI.eval(CG);
					exp->eval(CG);
					bool result = (dynamic_cast<PDTBoolConst*>(exp->nValue))->getValue();
					if (result)
					{
						cout<<"Quantifier there exits satisfied"<<endl;
						nValue = new PDTBoolConst(CG, false);
						return true;
					}
				}
			}
		}
		cout<<"Quantifier there exists is not satisfied"<<endl;
		nValue = new PDTBoolConst(CG, true);
		return true;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "ThereExist ";
		PDTQuantifier::toString(ss);
		return ss;
	}
};
